% !TEX root = eventadapt-post.tex


\appendix
\section{Reduction Semantics: Full Set of Rules\label{app:opsem}}
Table \ref{tab:redsem-full} gives the full set of reduction semantics rules.
\begin{table}[h!]
\[
\begin{array}{lc}
 \rulename{r:Open} & 
\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\STT}.Q} \pired \hfill  \\
& \hfill 
\restr{\cha}{\big({\locc{P\sub{\cha^{p}}{x} \para \que{\cha^p}{\ST}}  \para  \locd{Q\sub{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT} }\big) } \quad (\ST \cdual \STT) \vspace{1.5mm} \\

\rulename{r:Com} &
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\STT}}} 
\pired \hfill \\
&\hfill
\locc{P \para \que{\cha^p}{\ST}} \para  \locd{Q\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\STT} } 
%\quad (\ST \cdual \STT) %\quad ({e} \downarrow {c}) 
\vspace{1.5mm}
\\
%\rulename{r:Sel} &
%C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
%& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
%\pired \\
%& 
%\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  
\rulename{r:Sel} &
\locc{\branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J}\! \para\!  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}}}\! \para \!
\locd{\select{\cha^{\,\overline{p}}}{n_i};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\STT_j \}_{j \in J}} } \\
& \hfill \pired   C\{P_i \para \que{\cha^p}{\ST_i} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\STT_i} \}  
\quad (%\ST_i \cdual \STT_i,\, 
i \in J)  
\vspace{1.5mm}
\\
\rulename{r:Clo} &
\locc{\close{\cha^{\,p}}.P \para \que{\cha^p}{\tend} } \para  \locd{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\tend}} \pired %\\
%& \hfill 
\locc{P} \para  \locd{Q} \vspace{ 2mm}
\\
\rulename{r:Eva} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{1.5mm}\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{1.5mm}
\\
%\rulename{r:Con} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
%\vspace{1.5mm}\\
%  \rulename{r:Loc} &
% \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{1.5mm}
% \\ 
\rulename{r:ResN} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
\vspace{1.5mm}\\
\rulename{r:ResC} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{1.5mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{1.5mm}
\\
 \rulename{r:Rec} &
\recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}
\vspace{1.5mm}\\
\rulename{r:IfTrue} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{1.5mm}
\\
 \rulename{r:IfFalse} &
\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{1.5mm}\\
\rulename{r:UReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{\mathbf{0}}
\vspace{2mm}\\
\rulename{r:Arr1} & 
\displaystyle\frac{ \til{r} =  r_1 \cdot \til{r_0} }{
\locc{\evc{E}[\arrive{\locf{loc},r_1}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{true}]}
\para \locd{\que{\locf{loc}}{\til{r_0}}} }  
\vspace{2mm}\\
\rulename{r:Arr2} & \displaystyle\frac{ (\til{r} = r_2 \cdot \til{r_0}  \land r_1 \neq r_2) \lor \til{r} = \epsilon}{
\locc{\evc{E}[\arrive{\locf{loc},r_1}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{false}]}
\para \locd{\que{\locf{loc}}{\til{r}}} }  
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:UpdOld} & 
%\displaystyle\frac{
%\begin{array}{rcl} 
%\multicolumn{3}{c}{\mathsf{fc}(P)  = \cha_1^p, \ldots, \cha^p_n }
%%& &
%%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
%\\
% (V = P \land R' = R) & \bigvee  & \big(
% \mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) ~ \land~
%\\ 
%&& ~~~ V = Q_l\subst{\til{\cha}\,}{\,\til{x}_0} ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para\! \cdots\! \para \que{\cha^p_n}{\STT^{l}_n} 
%  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P \para R}} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V \para R'}} \para \locd{\mathbf{0}}
%\end{array}
%} 
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{r:Upd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\multicolumn{3}{c}{\mathsf{fc}(P) = \{ \cha_1^p, \ldots, \cha^p_m \} \qquad \forall j \in [1,..,m]. (\Pin{P}{\que{\cha^p_j}{\ST_j}})}
%& &
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
\\
 (V = P) & \bigvee  & \exists l.\big(
 \mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) ~ \land~
\\ 
&& \qquad V = Q_{l\,}\subst{\cha^p_1, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m} 
  \big)
\end{array}
}{
\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \quad  \\
\hfill \locc{\scomponent{\locf{loc}}{V}} \para \locd{\mathbf{0}}
\end{array}
} 
\end{array}
%\vspace{-3mm}
\]
\caption{Reduction Semantics: Full Set of Rules.
Above, $\ST$ and $\STT$ denote session types. % (cf. Def.~\ref{d:types})
\label{tab:redsem-full}}
%\vspace{-7mm}
\end{table}
\newpage
\section{Type System: Additional Typing Rules}\label{ap:adtyping}
Table \ref{t:addtyperules} gives additional typing rules for the system in \S\,\ref{s:types}.

\begin{table}[!h]
{\small
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:bool}]
{\typing{\Gamma}{\true, \false}{\bool}}{} 
\qquad
\infer[\rulename{t:name}]
{\typing{\Gamma}{u}{\name}}{} 
\vspace{1.5mm} \\
\infer[\rulename{t:bVar}]
{\typing{\Gamma, x: \bool }{x}{\bool}}{} 
\qquad
\infer[\rulename{t:nVar}]
{\typing{\Gamma, x: \name}{x}{\name}}{} 
\vspace{1.5mm} \\
\infer[\rulename{t:eq}]
{\typing{\Gamma}{d=d}{\bool}}{d=u \vee d=\kappa^p \vee d =x} \qquad 
\infer[\rulename{t:Ser}]
{\typing{\Gamma, u:\langle\ST_\qua, {\STT}_\qua\rangle}{u}{\langle\ST_\qua, {\STT}_\qua\rangle}}{\ST \cdual \STT } 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{1.5mm} \\
%\inferrule*[right=\rulename{t:Accept}]
%{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \quad \gamma \csub \alpha \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: \gamma_\qual}}}
%\vspace{1.5mm} \\
%\inferrule*[right=\rulename{t:Request}]
% {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \quad \gamma \csub \STT \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma }{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: {\gamma}_\qual }}} 
%\vspace{1.5mm} \\
%\inferrule*[right=\rulename{t:Clo}]
% {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\tend}{ \INT}}}
%\quad
%\inferrule*[right=\rulename{t:Par}]
% {
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
% }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
%
%\vspace{1.5mm} \\
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
\qquad
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:In}]
{\judgebis{\env{\Gamma, {x}:{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{{x}}.P }{\type{\ActS, k:?({\capab}).\ST}{ \INT}}}
\quad 
\inferrule*[right=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \typing{\Gamma}{e}{\capab}}
{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{{e}}.P}{\type{\ActS, k:!({\capab}).\ST}{ \INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Weakc}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
 
\quad
\inferrule*[right=\rulename{t:Weakn}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad u \notin dom(\INT)}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT }}}


\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:If}]
 {
 \typing{\env{\Gamma}{\Theta}}{ e}{\mathsf{bool}} \qquad 
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad 
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$
}
\caption{Additional Typing Rules.\label{t:addtyperules}}
\end{table}